[e1;e2]~([a,b].p(a;b))*[a,b].q(a;b)
== m:, f:(m{e:E| loc(e) = loc(e1) }).
== f(0) = e1 & f(m-1)  e2 
== & (i:(m-1). (f(i) <loc f(i+1))) & (i:(m-1). p(f(i);pred(f(i+1))))
== & q(f(m-1);e2) 

latex

---

clarification:

es-pstar-q(es;a,b.p(a;b);a,b.q(a;b);e1;e2)
== m:, f:({0..m}{e:es-E(es)| es-loc(es; e) = es-loc(es; e1)  Id }).
== f(0) = e1  es-E(es) & es-le(es;f(m-1);e2)
== & (i:{0..(m-1)}. es-locl(es; (f(i)); (f(i+1))))
== & (i:{0..(m-1)}. p(f(i);es-pred(es; (f(i+1)))))
== & q(f(m-1);e2) 

latex

Definitions	[e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), , x:A. B(x), Id, loc(e), E, e  e' , P & Q, (e <loc e'), x:A. B(x), {i..j}, pred(e)
FDL editor aliases	es-pstar-q